Nuprl Lemma : divides_mul
2,24
postcript
pdf
a
,
b
:
.
a
|
b
(
n
:
.
n
a
|
n
b
)
latex
Definitions
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
Prop
Lemmas
divides
wf
origin
a, b:
. a | b 
(n:. n
a | nb) a, b:. a | b (n:. na | nb) Qx:A. B(x)
T
x:A. B(x)